{-
 -  Separ, Type/Quantifiers.hs
 -
 -  Copyright (c) 2010 Dariusz Leniowski. All Rights Reserved.
 -
 -  Redistribution and use in source and binary forms, with or without 
 -  modification, are permitted provided that the following conditions 
 -  are met:
 -
 -  1. Redistributions of source code must retain the above copyright 
 -     notice, this list of conditions and the following disclaimer.
 -
 -  2. Redistributions in binary form must reproduce the above copyright 
 -     notice, this list of conditions and the following disclaimer 
 -     in the documentation and/or other materials provided with 
 -     the distribution.
 -
 -  3. The name of the author may not be used to endorse or promote 
 -     products derived from this software without specific prior 
 -     written permission.
 -
 -  THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS 
 -  "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT 
 -  LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS 
 -  FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL 
 -  THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, 
 -  INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES 
 -  (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS 
 -  OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) 
 -  HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, 
 -  STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING 
 -  IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE 
 -  POSSIBILITY OF SUCH DAMAGE.
 -
 -}

{-# LANGUAGE FlexibleContexts,UndecidableInstances,PatternGuards #-}

-- Module Quantifiers
-- Quantification
--   instances of Quantifiable (Type,Formulae)
--     quantify, unquantify
-- Lambdable (makeLam function)
--   function to convert any type to lambda expression if possible
--
   
module Type.Quantifiers where

import Prelude hiding (gcd)
import qualified Data.IntSet as RefSet
import qualified Data.List as List
import Control.Monad

import Type.Base
import Type.ClsType
import Type.ClsData hiding (t)
import Type.Lattice

type RefSet = RefSet.IntSet

---------------------------------------------------------------------
-- Quantify and Unquantify (skolemize, instantiate and forallize)
---------------------------------------------------------------------
--
--  skolemize   = unquantify true
--  instantiate = unquantify false
--  forallize   = quantify
--
--  class Quantifiable a where
--      quantify :: FInfo -> a -> MM a
--      unquantify :: Bool -> a -> MM (a,FInfo)
--
--  unquantify removes top-level quantifier (Var or Qua Bool) if present
--    and returns data (finfo) so adequate 
--    requantification will be possible
--  quantify is the inverse of unquantify
--

instance Ensurable Formulae => Quantifiable Type where
	unquantify _ t@(Cls _) = return (t,FInfo [])
	unquantify _ t@(Ref _) = return (t,FInfo [])
	unquantify _ t@(Lca _ _) = return (t,FInfo [])
	unquantify _ t@(Gcd _ _) = return (t,FInfo [])
	unquantify _ t@(Lam _ _ _) = return (t,FInfo [])
	unquantify q   (Var r b f s) = do
		mr <- testRefFree r
		let (r',f',s') = case mr of
			Nothing -> (r,f,s)
			Just r'' -> let g = subRef r (Ref r'') in (r'',substy g f, substy g s)
		newVar q r' b f' r'
		-- here f' should be ensured, but this will be done in normalize FInfo
		return (s',FInfo [(q,r')])
	unquantify _   (App _ _ _) = error $ "unquantify got App"
	unquantify _ t@(PSet _ _ _) = return (t,FInfo [])
	unquantify _ t@(PGet _ _) = return (t,FInfo [])

	quantify (FInfo []) t = return t
	-- skip quantifiers for constant terms (independent of vars)
	quantify (FInfo ((_,x):xs)) t | typeIsConstant t = do 
		ch <- getVarChildren x
		handleFormulae [] [x]
		_ <- quantify' (Var) ch t 
		quantify (FInfo xs) t
	quantify (FInfo ((_,x):xs)) t = do 
		ch <- getVarChildren x
		handleFormulae [] [x]
		quantify' (Var) ch t >>= quantify (FInfo xs)
					
instance Ensurable Formulae => Quantifiable Formulae where
	unquantify _ f@(TT) = return (f,FInfo [])
	unquantify _ f@(FF) = return (f,FInfo [])
	unquantify _ f@(And _) = return (f,FInfo [])
	unquantify _ f@(Eq _ _) = return (f,FInfo [])
	unquantify _ f@(Leq _ _ _) = return (f,FInfo [])
	unquantify q   (Qua q2 r b f1 f2) | q == q2 = do
		mr <- testRefFree r
		let (r',f1',f2') = case mr of
			Nothing -> (r,f1,f2)
			Just r'' -> let g = subRef r (Ref r'') in	(r'',substy g f1, substy g f2)
		newVar q r' b f1' r'
		-- here f1' should be ensured, but this will be done in normalize FInfo
		return (f2',FInfo [(q,r')])
	unquantify q1   (Qua q2 _ _ _ _) = 
		fail $ "unquantify got " ++ show q1 ++ " Qua " ++ show q2

	quantify (FInfo []) f = return f
	quantify (FInfo ((q,x):xs)) f | formulaeIsConstant f = do -- TT or FF
		ch <- getVarChildren x
		handleFormulae [] [x] -- there is no problem with skolems
							  -- since all children of x are skolems too
		_ <- quantify' (Qua q) ch f 
		quantify (FInfo xs) f -- old f since it is constant
	quantify (FInfo ((q,x):xs)) f = do 
		ch <- getVarChildren x
		handleFormulae [] [x] -- there is no problem with skolems
								-- since all children of x are skolems too
		quantify' (Qua q) ch f >>= quantify (FInfo xs)

-- functions used by quantify Type and quantify Formulae
--
-- handleFormulae gathers all formulae from var and its children
-- and traverses them for used references and assign them at
-- proper places e.g.
-- (forall x (no,th) TT (forall y (no,th) (x = C) t)) 
-- will become
-- (forall x (no,th) (x=C) (forall y (no,th) C))
handleFormulae :: Ensurable Formulae => [Formulae] -> [RefType] -> MM ()
handleFormulae fs [] = segregate (And fs) where
	segregate TT = return ()
	segregate FF = fail $ "handleFormulae got FF"
	segregate (And ls) = mapM_ segregate ls
	segregate f = do
		vs <- uniGetVars f RefSet.empty
		if RefSet.null vs then ensure f else do
			let m mx my = do 
				(_,tx) <- mx
				(_,ty) <- my
				if tx < ty then my else mx
			let n x = do t <- getVarTimeTags x; return (x,t)
			(y,_) <- foldr1 m $ map n $ RefSet.toList vs
			getVarFormulae y >>= (setVarFormulae y . fand f)
handleFormulae fs (x:xs) = do
	f <- getVarFormulae x
	setVarFormulae x TT
	ch <- getVarChildren x
	handleFormulae (f:fs) $ List.delete x ch ++ xs

-- core of quantify
-- build is a constructor
quantify' :: (SubstitutableM b) =>
             (RefType -> (Type, Type) -> Formulae -> b -> b)
             -> [RefType] -> b -> MM b
quantify'     _    []  tf = return tf
quantify' build (x:xs) tf = do
	-- TODO (here and in Formulae)
	-- here it should be possilbe to handle recursive terms
	-- like (Var x (no,th) (Eq x <term(x)>) t)
	-- if not, code an occur check
	-- UPDATE occur check coded, but 
	-- recursive terms would be nice, wouldn't they?
	p <- getVarParent x
	delVarChild p x
	ch <- getVarChildren x
	tf' <- quantify' build ch tf
	-- it is important for all this to be done before delVarData
	d <- getVarData x
	guard $ List.null $ children d -- TODO remove
	free <- isVarFree x
	-- occur check (if x is free nothing happens)
	_ <- occurCheck (Ref x)
	-- before crossing the Rubicon
	delVarData x
	-- alea iacta est
	if free then quantify' build xs (build x (bounds d) (formulae d) tf')
	        else substyM (subRef x $ value d) tf' >>= quantify' build xs
			
			
-----------------------------------------------
-- MAKE LAMBDA
-----------------------------------------------
--
-- converts any type to lambda expression (but sometimes fails)
-- makeLam quantifier direction type
--   quantifier is how lambda expression should be dealt when
--   unquantifying (e.g. when resolving subtypes form classes)
-- returns (argument,result,finfo)
--   finfo is info returned from unquantify
--
--  class Lambdable a where
--      makeLam :: Bool -> Bool -> a -> MM (a,a,FInfo)
--

instance (Evaluable Type,Quantifiable Type) => Lambdable Type where
	makeLam q b t@(App _ _ _) = eval t >>= makeLam q b -- hope it won't hurt
	makeLam q b t@(Var _ _ _ _) = do
		(t',i) <- unquantify q t
		(a,r,vs) <- makeLam q b t'
		return (a,r,vs +++ i)
	makeLam _ b (Lam c a r) = 
		if b == c then return (a,r,FInfo [])	
		else fail $ "" -- "got LamLeft <-> LamRight"
	makeLam q b (Gcd c d) = do
		(ca,cr,cv) <- makeLam q b c
		(da,dr,dv) <- makeLam q b d
		return (Lca ca da,Gcd cr dr,cv+++dv)
	makeLam q b (Lca c d) = do
		(ca,cr,cv) <- makeLam q b c
		(da,dr,dv) <- makeLam q b d
		return (Gcd ca da,Lca cr dr,cv+++dv)
	makeLam q b (Ref r) = do
		i <- isVarInst r
		s <- isVarSkolem r
		if s then do
				(_,th) <- getVarBounds r
				makeLam q b th -- TODO is this allright?
			else if i then do
				(no,th) <- getVarBounds r
				(na,nr,nv) <- makeLam q b no
				(ta,tr,tv) <- makeLam q b th
				x <- uniqRef
				y <- uniqRef
				-- r is Inst, so are x and y
				newVarInst x (ta,na) TT r
				newVarInst y (nr,tr) TT r
				setVarValue r (Lam b (Ref x) (Ref y))
				-- nv and tv were added by makeLam
				-- therefore have no corresponding forVar
				-- so are returned here; x and y will be
				-- forallized the place r would have been
				return (Ref x,Ref y,nv+++tv) 
			else do
				v <- getVarValue r
				makeLam q b v
	makeLam q b (PSet u n v) | (Cls c) <- getcls u = 
		clsGetSubtype c (PSet u n v) >>= makeLam q b where
			getcls (PSet u n v) = getcls u
			getcls u = u
	makeLam q b (PSet u n v) = do
		(a,r,i) <- makeLam q b u
		return (a,pSet r n v,i)
	makeLam q b (PGet u n) = evalProperty n u >>= makeLam q b
	makeLam _ _ (Cls c) | clsIsThingNothing c = 
		return (typeNothing, typeThingNothing, FInfo [])
	makeLam _ _ (Cls c) | clsIsNothingThing c = 
		return (typeThing, typeNothingThing, FInfo [])
	makeLam _ _ (Cls c) | clsIsThing c = 
		return (typeNothing, typeThing, FInfo [])
	makeLam _ _ (Cls c) | clsIsNothing c = 
		return (typeThing, typeNothing, FInfo [])
	makeLam q b (Cls c) = clsGetSubtype c (Cls c) >>= makeLam q b

